/*
 * Copyright 2011, 2012 Fabian Wenzelmann
 * 
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 * 
 * Recognition-Procedures-for-Boolean-Functions is free software: you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation, either version 3 of the License, or
 * (at your option) any later version.
 * 
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 * 
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.  If not, see <http://www.gnu.org/licenses/>.
 */

package de.wenzelmf.booleanFunction.lpb.combinatorial.splittingTree;

import org.w3c.dom.Document;
import org.w3c.dom.Element;

import de.wenzelmf.booleanFunction.dnf.Clause;
import de.wenzelmf.booleanFunction.dnf.ClauseFactory;
import de.wenzelmf.booleanFunction.dnf.DNF;
import de.wenzelmf.booleanFunction.dnf.DNFFactory;
import de.wenzelmf.booleanFunction.lpb.combinatorial.occurrencePattern.OccurrencePattern;
import de.wenzelmf.booleanFunction.lpb.combinatorial.occurrencePattern.OccurrencePatternFactory;
import de.wenzelmf.booleanFunction.lpb.util.LPBCombinatorialConstants;
import de.wenzelmf.booleanFunction.util.Tuple;

/**
 * Class representing the main nodes in the splitting tree.
 * 
 * @author Fabian Wenzelmann
 * @version 1.0
 *
 */
public class MainNode extends SplittingTreeNode
{
	/*
	 * The maximal <i>l</i> value such that the first <i>l</i> occurrence patterns are equal.
	 */
	private int maxL;
	/*
	 * Value is set to true if this is a final main node (i.e. true if it's DNF is true or false).
	 */
	private boolean isFinal;
	
	/**
	 * Construct a new main node.
	 * 
	 * @param lowerParent The lower parent of the node (referring to the table representation).
	 * @param upperParent The upper parent of the node (referring to the table representation).
	 * @param dnf The DNF associated with this node.
	 * @param occurrencePatterns The occurrence patterns (for all variables that have not been split away yet),
	 * variables are sorted according the relation on occurrence patterns.
	 * @param context Information about the tree this node is used in.
	 * 
	 */
	public MainNode(SplittingTreeNode lowerParent,
			SplittingTreeNode upperParent, DNF dnf,
			OccurrencePattern[] occurrencePatterns, TreeContext context)
	{
		super(lowerParent, upperParent, dnf, occurrencePatterns, context);
		this.isFinal = calcIsFinal();
		maxL = -1;
	}
	
	/**
	 * Construct a new main node, the parameter {@code isFinal} should be {@code true} iff
	 * {@code dnf} represents either <i>true</i> or <i>false</i>.
	 * 
	 * @param lowerParent The lower parent of the node (referring to the table representation).
	 * @param upperParent The upper parent of the node (referring to the table representation).
	 * @param dnf The DNF associated with this node.
	 * @param occurrencePatterns The occurrence patterns (for all variables that have not been split away yet),
	 * variables are sorted according the relation on occurrence patterns.
	 * @param context Information about the tree this node is used in.
	 * @param isFinal {@code true} iff {@code dnf} represents either <i>true</i> or <i>false</i>.
	 */
	public MainNode(SplittingTreeNode lowerParent,
			SplittingTreeNode upperParent, DNF dnf,
			OccurrencePattern[] occurrencePatterns, TreeContext context,
			Boolean isFinal)
	{
		super(lowerParent, upperParent, dnf, occurrencePatterns, context);
		this.isFinal = (isFinal == null ? calcIsFinal() : isFinal);
		maxL = -1;
	}

	/**
	 * Implements the {@code split} method for main nodes.
	 * 
	 * This method first calculates the maximal <i>l</i> value s.t. the first <i>l</i> occurrence
	 * patterns are equal. After calling this method {@link #getMaxL()} should return a value != -1.
	 * 
	 * Depending on this l value it creates again main nodes or auxiliary nodes.
	 */
	@Override
	public void split(boolean symmetryTest, OccurrencePatternFactory factory, VariableSetting variables,
			ClauseFactory clauseFactory, DNFFactory dnfFactory) throws NotSymmetricException
	{
		// get max l value
		this.maxL = getMaxL(variables);
		this.alreadySplit = true;
		
		Tuple<SplitResult, SplitResult> splitResult = splitBoth(factory, variables,
				clauseFactory, dnfFactory);
		SplitResult first = splitResult.getFirst();
		SplitResult second = splitResult.getSecond();
		
		if(maxL == 1)
		{
			this.upperChild = new MainNode(this, null, first.dnf, first.patterns, context, first.isFinal);
			this.lowerChild = new MainNode(null, this, second.dnf, second.patterns, context, second.isFinal);
		}
		else
		{
			this.upperChild = new AuxiliaryNode(this, null, first.dnf, first.patterns, 
					context, maxL, 1);
			this.lowerChild = new AuxiliaryNode(null, this, second.dnf, second.patterns,
					context, maxL, 1);
		}
	}
	
	/**
	 * Calculates the maximal <i>l</i> value s.t. the first <i>l</i> occurrence patterns are equal.
	 * 
	 * This method returns at least 1 (because of the first variable).
	 * 
	 * @param variables The variable setting that gives us some global information about the variables.
	 * 
	 * @return The maximal <i>l</i> value s.t. the first <i>l</i> occurrence patterns are equal.
	 */
	protected int getMaxL(VariableSetting variables)
	{
		int l = 1;
		OccurrencePattern[] patterns = getOccurrencePatterns();
		// must exist!
		OccurrencePattern first = patterns[0];
		/*if(first == null)
		{
			// TODO: Strange behavior if the DNF cannot be represented as a LPB
			// first can be null in this case?
			// why?
		}*/
		//while(l < patterns.length && patterns[l] != null)
		while(l < patterns.length)
		{
			if(patterns[l] == null)
			{
				// TODO: is this correct?
				// should be... if no occurrence pattern has been created the variable does not
				// occur and therefore the OP should be empty
				patterns[l] = LPBCombinatorialConstants.defaultOPFactory.getEmptyInstance((variables.getVariable(column + l)));
			}
			if(first.equals(patterns[l]))
			{
				l++;
			}
			else
			{
				break;
			}
		}
		
		return l;
	}

	/**
	 * Return {@code true} if the node is final, i.e. the DNF of this node is true or false.
	 * 
	 * @return {@code true} if the node is final.
	 */
	@Override
	public boolean isFinal()
	{
		return isFinal;
	}
	
	/**
	 * Returns the type of the node, that is "mainNode".
	 * 
	 * @return "mainNode".
	 */
	@Override
	public String getType()
	{
		return "mainNode";
	}
	
	// TODO: can we speed it up?
	// we have to check each clause... that is quite inefficient (in general)
	// maybe find it out while creating the DNF?
	/**
	 * Return {@code true} if this node is final, i.e. the DNF is true or false.
	 * 
	 * @return {@code true} if the DNF of this node is true or false.
	 */
	private boolean calcIsFinal()
	{
		if(dnf.size() == 0)
			return true;
		else if(dnf.size() == 1)
		{
			for(Clause c : dnf)
			{
				if(c.size() == 0)
					return true;
			}
		}
		return false;
	}
	
	/**
	 * Create a String representation of this node.
	 * 
	 * @return "Main Node: " + dnf.toString().
	 */
	@Override
	public String toString()
	{
		return "Main Node: " + dnf;
	}

	/**
	 * Return the maximal <i>l</i> value such that the first <i>l</i> occurrence patterns are equal.
	 * 
	 * It returns -1 as long as none if the {@code split} methods has been called.
	 * 
	 * @return The maximal <i>l</i> value such that the first <i>l</i> occurrence patterns are equal.
	 */
	public int getMaxL()
	{
		return maxL;
	}
	
	/**
	 * Return a XML element representing this node as defined in the manual.
	 *  
	 * @param document The root document (use it to create the Element object).
	 * 
	 * @return An element representing this node as defined in the manual.
	 */
	public Element getXMLElement(Document document)
	{
		Element result = super.getXMLElement(document);
		
		result.setAttribute("maxL", "" + getMaxL());
		result.setAttribute("isFinal", "" + isFinal());
		
		return result;
	}
}
